Inference at * 2 1 1 1 
Iof proof for Lemma primrec add:

.....falsecase..... NILNIL

1. T : Type
2. n : 
3. 0 < n
4. m:, b:T, c:({0..((n - 1)+m)}TT).
4. primrec((n - 1)+m;b;c) = primrec(n - 1;primrec(m;b;c);i,t. c(i+m,t))
5. m : 
6. b : T
7. c : {0..(n+m)}TT
8. b' : T
9. primrec(m;b;c) = b'
10. primrec((n - 1)+m;b;c) = primrec(n - 1;b';i,t. c(i+m,t))
11. (n+m = 0)
12. (n = 0)
  c(((n+m) - 1),primrec((n+m) - 1;b;c)) = c((n - 1)+m,primrec(n - 1;b';i,t. c(i+m,t))) 

latex

 by ((Subst' ((n+m) - 1) = (n - 1)+m 0) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 1000:n)) (first_tok SupInf:t) inil_term))) 

latex

C1: 

C1:   c((n - 1)+m,primrec((n - 1)+m;b;c)) = c((n - 1)+m,primrec(n - 1;b';i,t. c(i+m,t)))
C.

Definitions	, t  T, {T}, P  Q, SQType(T), x:A. B(x), False, A,
Lemmas	guard wf